Nuprl Definition : es-first-at-since' 0,22
es-first-at-since'(es;i;e;e.R(e);e.P(e))
== loc(e) = i
== & R(e)
== & (e':E. (e' <loc e) & P(e') & (e'':E. e'  e''   (e'' <loc e)  R(e''))) 
latex

clarification:

es-first-at-since'(es;i;e;e.R(e);e.P(e))
== es-loc(es; e) = i  Id
== & R(e)
== & (e':es-E(es).
== & (es-locl(es; e'; e)
== & (& P(e') & (e'':es-E(es). es-le(es;e';e'')  es-locl(es; e''; e)  R(e''))) 
latex

Definitionses-first-at-since'(es;i;e;e.R(e);e.P(e)), Id, loc(e), x:A. B(x), A & B, P & Q, x:A. B(x), E, e  e' , P  Q, (e <loc e'), A
FDL editor aliaseses-first-at-since'

origin